// SPDX-License-Identifier: GPL-2.0 or GPL-3.0
// Copyright © 2019 Ariadne Devos

#ifndef _sHT_MATH_EXPNAT_POWER10_H
#define _sHT_MATH_EXPNAT_POWER10_H

#include <sHT/math/expnat.h>

// Desc: numeric values of common powers of 10
//   > Useful for overflow checking.
//   > These take a little computative effort.
// Proof status: auto
// Proof method: compute
/*@ axiomatic Exp10 {
      // 1 thousand
      lemma exp10_3: expnat(10, 3) == 1000;
      // 1 million
      lemma exp10_6: expnat(10, 6) == 1000000;
      // 1 milliard (being unambigious yet concise)
      // (slightly less than UINT32_MAX)
      lemma exp10_9: expnat(10, 9) == 1000000000;
    } */

#endif
